//  /=============================================================/
//  |   Auteurs  : J.JULLIEN / R.HERLEMAN / R.CHAILAN             |
//  |   Fichier  : matrice.h                                      |
//  |   Date     : 10/04/2009                                     |
//  |   Objet    : Spécification du type "t_MatriceCreuse" &      |
//  |              ses fonctions associées                        |
//  /=============================================================/

#include <stdio.h>
#include <stdlib.h>

#include "clause.h"
#include "variable.h"

/* ------------------------------------------------------------------------ */
/* ---------------------- Déclaration types exportés ---------------------- */
/* ------------------------------------------------------------------------ */

typedef struct t_MatriceCreuse {
  t_Clause* clauses;
  t_Variable* variables;
  int nbClauses;
  int nbVariables;
  
  int nbSatisfaites;
  int nbFalsifiees;
  int nbInchangees;
  int nbRaccourcies;
  
  int valeurAChoisir;
  
  int minNbNeutres;        // minNbNeutres = min { i ∈ [1, ..., nbVariables-1]
                           // tq hashClauses[i] ≠ NULL }
  t_Clause** hashClauses;  // Table de hashage des clauses (doublement
                           // chaînées) par leur nombre de litteraux neutres
} t_MatriceCreuse;

/* ------------------------------------------------------------------------ */
/* -------------------- Déclaration fonctions exportés -------------------- */
/* ------------------------------------------------------------------------ */

/*----------------------------------------------------------------------------
Nom              : matriceSetVariableAChoisir
Prérequis        : val ∈ {0, 1}
Action           : Cette fonction permet de définir la premiere valeur de
                   variable à choisir dans l'algorithme de résolution
Type de retour   : -
Variable(s)      :
  E/S t_MatriceCreuse*   mC - Ensemble de clauses
  E   int                val - val ∈ {0, 1}
----------------------------------------------------------------------------*/
void matriceSetVariableAChoisir (t_MatriceCreuse *mC, int val);

/*----------------------------------------------------------------------------
Nom              : matriceCreerDepuisFichier
Prérequis        : Le fichier respecte le format décrit dans le sujet en
                   annexes
Action           : Retourne une matrice creuse contenant l'ensemble des
                   clauses décrites dans le fichier f
Type de retour   : t_MatriceCreuse
Variable(s)      :
  E/S FILE*   f - Descripteur de fichier sur le fichier de clauses, ouvert en
                  lecture
----------------------------------------------------------------------------*/
t_MatriceCreuse matriceCreerDepuisFichier (FILE* f);

/*----------------------------------------------------------------------------
Nom              : matriceResolution
Prérequis        : La matrice est initialisée de façon correcte
Action           : Retourne vrai si l'ensemble de clauses possède au moins
                   une solution, faux sinon
Type de retour   : int (0 ou 1)
Variable(s)      :
  E/S t_MatriceCreuse*   mC - Ensemble de clauses à résoudre
----------------------------------------------------------------------------*/
int matriceResolution (t_MatriceCreuse *mC);

/*----------------------------------------------------------------------------
Nom              : matriceVerifierAffectation
Prérequis        : Le fichier respecte le format décrit dans le sujet en
                   annexes, et mC est correctement initialisé
Action           : Retourne vrai si l'affectation des solutions de mC
                   satisfait toute les clauses
Type de retour   : int (0 ou 1)
Variable(s)      :
  E   t_MatriceCreuse*   mC - Ensemble des clauses à tester
  E/S FILE*   f - Descripteur de fichier sur le fichier de clauses, ouvert en
                  lecture
----------------------------------------------------------------------------*/
int matriceVerifierAffectation (t_MatriceCreuse mC, FILE* f);

/*----------------------------------------------------------------------------
Nom              : matriceEstResolue
Prérequis        : -
Action           : Retourne vrai si toutes les clauses de mC sont satisfaites
Type de retour   : int (0 ou 1)
Variable(s)      :
  E   t_MatriceCreuse   mC - Ensemble des clauses à tester
----------------------------------------------------------------------------*/
int matriceEstResolue (t_MatriceCreuse mC);

/*----------------------------------------------------------------------------
Nom              : matriceAfficherMatrice
Prérequis        : -
Action           : Affiche la matrice en version "graphique/2D"
Type de retour   : -
Variable(s)      :
  E   t_MatriceCreuse   mC - Ensemble des clauses à afficher
----------------------------------------------------------------------------*/
void matriceAfficherMatrice (t_MatriceCreuse mC);

/*----------------------------------------------------------------------------
Nom              : matriceAfficherEnsemble
Prérequis        : -
Action           : Affiche la matrice en version ensemble de clauses
Type de retour   : -
Variable(s)      :
  E   t_MatriceCreuse   mC - Ensemble des clauses à afficher
----------------------------------------------------------------------------*/
void matriceAfficherEnsemble (t_MatriceCreuse mC);

/*----------------------------------------------------------------------------
Nom              : matriceAfficherFormule
Prérequis        : -
Action           : Affiche la matrice en version formule logique
Type de retour   : -
Variable(s)      :
  E   t_MatriceCreuse   mC - Ensemble des clauses à afficher
----------------------------------------------------------------------------*/
void matriceAfficherFormule (t_MatriceCreuse mC);

/*----------------------------------------------------------------------------
Nom              : matriceAfficherDebug
Prérequis        : -
Action           : Affiche des informations détaillées sur la matrice
Type de retour   : -
Variable(s)      :
  E   t_MatriceCreuse   mC - Ensemble des clauses à afficher
----------------------------------------------------------------------------*/
void matriceAfficherDebug (t_MatriceCreuse mC);

/*----------------------------------------------------------------------------
Nom              : matriceAfficherSimplifiee
Prérequis        : -
Action           : Affichage de l'ensemble des clauses courant sous forme
                   simplifiée (on ne fera pas figurer dans l'affichage les
                   clauses satisfaites, ni dans les autres clauses, les
                   litteraux qui ne sont pas neutres)
Type de retour   : -
Variable(s)      :
  E   t_MatriceCreuse   mC - Ensemble des clauses à afficher
----------------------------------------------------------------------------*/
void matriceAfficherSimplifiee (t_MatriceCreuse mC);

/*----------------------------------------------------------------------------
Nom              : matriceAfficherValeurs
Prérequis        : -
Action           : Affiche les valeurs des variables
Type de retour   : -
Variable(s)      :
  E   t_MatriceCreuse   mC - Ensemble des clauses à afficher
----------------------------------------------------------------------------*/
void matriceAfficherValeurs (t_MatriceCreuse mC);
